Until now, when inside theories, we were using From mathcomp when referring to classical files and no prefix when referring to files from theories (same reasoning for other directories). I think it was necessary to make the CI goes through and, of course, as a developer, I got used to it as a piece of information when reading headers. Your PR shows that we can put prefixes everywhere and the CI still goes through, that looks more homogeneous butiIs there an advantage in having From prefixes everywhere? (I think that I am asking because of my lack of experience with the -Q option.)

-Q is the same as -R except that it makes From mandatory.
The main advantage I see to the uniform use of From is to make PR creating subpackages suc as #1349 much easier, otherwise they request the addition of a lot of From everywhere, making their diff completely unreadable. A side advantage is that if Coq people add a file in the prelude/Stdlib with the same name as one of ours, this avoids the conflict.
The small drawback is that we loose the documentation that "no From" means "in theories". We could recover it by using From mathcomp.analysis instead of From mathcomp, but not sure it's a good idea and it will somewhat minimize the first advantage (when spliting sub packages).

If you prefer, we could use From mathcomp.analysis to keep that information?

If you prefer, we could use From mathcomp.analysis to keep that information?

The discipline of keeping the local packages last is enough I think.